/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.role;

import caetus.modelChecking.variable.ModelVariable;
import caetus.pkcs11.tokenCapabilities.TokenCapabilities;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;

/**
 * Represents a session - entity that "governs" over other roles (actors). While
 * session technically also is a role, it works in a completely different way,
 * so it has its own special class.
 *
 * @author Josef Hertl
 */
public class ModelSession extends ModelRole {

    private Map<ModelActor, List<ModelVariable>> actorChannelMap = new HashMap<ModelActor, List<ModelVariable>>();

    /**
     * Does not require name, because that always is "session".
     *
     * @param capabilities The passed capabilities of the token.
     */
    public ModelSession(TokenCapabilities capabilities) {
        super("session", capabilities);
    }

    @Override
    public String makeRole() {
        String result = super.makeRoleStart();
        result += "def=\n\n";
        result += super.prepareLocalVariables();
        result += prepareInit();
        result += makeComposition();
        result += super.makeRoleEnd();
        return result;
    }

    @Override
    protected String prepareInit() {
        String result = "\n";
        if (findVariable("PrK") != null) {
            result += "init PrK := inv(PuK)\n";
        }
        return result;
    }

    /**
     * Generates composition for the session, based off its actors.
     *
     * @return hlpsl-ready string representation of the composition, including
     * the "composition" keyword.
     */
    private String makeComposition() {
        String result = "\ncomposition\n\n";
        boolean first = true;
        for (ModelActor actor : actorChannelMap.keySet()) {
            if (first) {
                result += "     ";
                first = false;
            } else {
                result += "  /\\ ";
            }
            result += actor.getName() + "(";
            List<ModelVariable> variableList = new LinkedList<ModelVariable>(actor.getGlobalVariableListNoChannels());
            for (int i = 0; i < variableList.size(); i++) {
                result += variableList.get(i).getVariableName() + ",";
            }
            List<ModelVariable> channelList = actorChannelMap.get(actor);
            result += channelList.get(0).getVariableName() + ","; //here we automatically presume there are exactly two channels
            result += channelList.get(1).getVariableName();
            result += ")\n";
        }
        return result;
    }

    /**
     * Adds channels from the actors to this session. The session saves them as
     * local variables.
     *
     * @param modelActor The actor who is generating and adding the channels
     * @param inputList The list with the two channels
     */
    public void addChannelsFromActor(ModelActor modelActor, List<ModelVariable> inputList) {
        actorChannelMap.put(modelActor, inputList);
        super.addToLocalVariables(inputList);
    }
}
